A:Type, P:(A).
(s:A. Dec(k:. (P(s,k))))
 (s:A, k:. Dec(P(s,k)))
 (s:A. Dec(v:. ((P(s,v)) & (n:. (n < v)  P(s,n))))) 

latex

Definitions	t  T, x:A. B(x), P  Q, i  j < k, {x:A| B(x)} , x:AB(x), f(a), a < b, x:A  B(x), False, n - m, Type, , A c B, Void, , left + right, P  Q, Dec(P), x.A(x), x. t(x), {T}, i  j , -n, n+m, x(s1,s2), A, #$n, {i..j}, x:A. B(x), s ~ t, A  B, P & Q,
Lemmas	ge wf, nat properties, decidable wf, decidable ex int seg, decidable not, int seg wf, nat wf, not wf, le wf